active(g(X)) → mark(h(X))
active(c) → mark(d)
active(h(d)) → mark(g(c))
mark(g(X)) → active(g(X))
mark(h(X)) → active(h(X))
mark(c) → active(c)
mark(d) → active(d)
g(mark(X)) → g(X)
g(active(X)) → g(X)
h(mark(X)) → h(X)
h(active(X)) → h(X)
↳ QTRS
↳ DependencyPairsProof
active(g(X)) → mark(h(X))
active(c) → mark(d)
active(h(d)) → mark(g(c))
mark(g(X)) → active(g(X))
mark(h(X)) → active(h(X))
mark(c) → active(c)
mark(d) → active(d)
g(mark(X)) → g(X)
g(active(X)) → g(X)
h(mark(X)) → h(X)
h(active(X)) → h(X)
MARK(d) → ACTIVE(d)
ACTIVE(g(X)) → H(X)
H(active(X)) → H(X)
MARK(h(X)) → ACTIVE(h(X))
ACTIVE(g(X)) → MARK(h(X))
ACTIVE(h(d)) → MARK(g(c))
G(active(X)) → G(X)
ACTIVE(h(d)) → G(c)
G(mark(X)) → G(X)
MARK(c) → ACTIVE(c)
ACTIVE(c) → MARK(d)
MARK(g(X)) → ACTIVE(g(X))
H(mark(X)) → H(X)
active(g(X)) → mark(h(X))
active(c) → mark(d)
active(h(d)) → mark(g(c))
mark(g(X)) → active(g(X))
mark(h(X)) → active(h(X))
mark(c) → active(c)
mark(d) → active(d)
g(mark(X)) → g(X)
g(active(X)) → g(X)
h(mark(X)) → h(X)
h(active(X)) → h(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
MARK(d) → ACTIVE(d)
ACTIVE(g(X)) → H(X)
H(active(X)) → H(X)
MARK(h(X)) → ACTIVE(h(X))
ACTIVE(g(X)) → MARK(h(X))
ACTIVE(h(d)) → MARK(g(c))
G(active(X)) → G(X)
ACTIVE(h(d)) → G(c)
G(mark(X)) → G(X)
MARK(c) → ACTIVE(c)
ACTIVE(c) → MARK(d)
MARK(g(X)) → ACTIVE(g(X))
H(mark(X)) → H(X)
active(g(X)) → mark(h(X))
active(c) → mark(d)
active(h(d)) → mark(g(c))
mark(g(X)) → active(g(X))
mark(h(X)) → active(h(X))
mark(c) → active(c)
mark(d) → active(d)
g(mark(X)) → g(X)
g(active(X)) → g(X)
h(mark(X)) → h(X)
h(active(X)) → h(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
H(active(X)) → H(X)
H(mark(X)) → H(X)
active(g(X)) → mark(h(X))
active(c) → mark(d)
active(h(d)) → mark(g(c))
mark(g(X)) → active(g(X))
mark(h(X)) → active(h(X))
mark(c) → active(c)
mark(d) → active(d)
g(mark(X)) → g(X)
g(active(X)) → g(X)
h(mark(X)) → h(X)
h(active(X)) → h(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
H(active(X)) → H(X)
Used ordering: Polynomial interpretation [25,35]:
H(mark(X)) → H(X)
The value of delta used in the strict ordering is 8.
POL(active(x1)) = 4 + (2)x_1
POL(H(x1)) = (2)x_1
POL(mark(x1)) = (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
H(mark(X)) → H(X)
active(g(X)) → mark(h(X))
active(c) → mark(d)
active(h(d)) → mark(g(c))
mark(g(X)) → active(g(X))
mark(h(X)) → active(h(X))
mark(c) → active(c)
mark(d) → active(d)
g(mark(X)) → g(X)
g(active(X)) → g(X)
h(mark(X)) → h(X)
h(active(X)) → h(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
H(mark(X)) → H(X)
The value of delta used in the strict ordering is 1/16.
POL(H(x1)) = (1/4)x_1
POL(mark(x1)) = 1/4 + (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
active(g(X)) → mark(h(X))
active(c) → mark(d)
active(h(d)) → mark(g(c))
mark(g(X)) → active(g(X))
mark(h(X)) → active(h(X))
mark(c) → active(c)
mark(d) → active(d)
g(mark(X)) → g(X)
g(active(X)) → g(X)
h(mark(X)) → h(X)
h(active(X)) → h(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
G(active(X)) → G(X)
G(mark(X)) → G(X)
active(g(X)) → mark(h(X))
active(c) → mark(d)
active(h(d)) → mark(g(c))
mark(g(X)) → active(g(X))
mark(h(X)) → active(h(X))
mark(c) → active(c)
mark(d) → active(d)
g(mark(X)) → g(X)
g(active(X)) → g(X)
h(mark(X)) → h(X)
h(active(X)) → h(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(active(X)) → G(X)
Used ordering: Polynomial interpretation [25,35]:
G(mark(X)) → G(X)
The value of delta used in the strict ordering is 8.
POL(active(x1)) = 4 + (2)x_1
POL(mark(x1)) = (2)x_1
POL(G(x1)) = (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
G(mark(X)) → G(X)
active(g(X)) → mark(h(X))
active(c) → mark(d)
active(h(d)) → mark(g(c))
mark(g(X)) → active(g(X))
mark(h(X)) → active(h(X))
mark(c) → active(c)
mark(d) → active(d)
g(mark(X)) → g(X)
g(active(X)) → g(X)
h(mark(X)) → h(X)
h(active(X)) → h(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(mark(X)) → G(X)
The value of delta used in the strict ordering is 1/16.
POL(mark(x1)) = 1/4 + (2)x_1
POL(G(x1)) = (1/4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
active(g(X)) → mark(h(X))
active(c) → mark(d)
active(h(d)) → mark(g(c))
mark(g(X)) → active(g(X))
mark(h(X)) → active(h(X))
mark(c) → active(c)
mark(d) → active(d)
g(mark(X)) → g(X)
g(active(X)) → g(X)
h(mark(X)) → h(X)
h(active(X)) → h(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
MARK(h(X)) → ACTIVE(h(X))
ACTIVE(g(X)) → MARK(h(X))
MARK(g(X)) → ACTIVE(g(X))
ACTIVE(h(d)) → MARK(g(c))
active(g(X)) → mark(h(X))
active(c) → mark(d)
active(h(d)) → mark(g(c))
mark(g(X)) → active(g(X))
mark(h(X)) → active(h(X))
mark(c) → active(c)
mark(d) → active(d)
g(mark(X)) → g(X)
g(active(X)) → g(X)
h(mark(X)) → h(X)
h(active(X)) → h(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(h(d)) → MARK(g(c))
Used ordering: Polynomial interpretation [25,35]:
MARK(h(X)) → ACTIVE(h(X))
ACTIVE(g(X)) → MARK(h(X))
MARK(g(X)) → ACTIVE(g(X))
The value of delta used in the strict ordering is 3/2.
POL(c) = 1/2
POL(active(x1)) = 2 + (4)x_1
POL(MARK(x1)) = (2)x_1
POL(g(x1)) = (1/2)x_1
POL(h(x1)) = (1/4)x_1
POL(mark(x1)) = 1/2 + (2)x_1
POL(d) = 4
POL(ACTIVE(x1)) = (2)x_1
g(active(X)) → g(X)
g(mark(X)) → g(X)
h(active(X)) → h(X)
h(mark(X)) → h(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
MARK(h(X)) → ACTIVE(h(X))
MARK(g(X)) → ACTIVE(g(X))
ACTIVE(g(X)) → MARK(h(X))
active(g(X)) → mark(h(X))
active(c) → mark(d)
active(h(d)) → mark(g(c))
mark(g(X)) → active(g(X))
mark(h(X)) → active(h(X))
mark(c) → active(c)
mark(d) → active(d)
g(mark(X)) → g(X)
g(active(X)) → g(X)
h(mark(X)) → h(X)
h(active(X)) → h(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(g(X)) → MARK(h(X))
Used ordering: Polynomial interpretation [25,35]:
MARK(h(X)) → ACTIVE(h(X))
MARK(g(X)) → ACTIVE(g(X))
The value of delta used in the strict ordering is 8.
POL(active(x1)) = (2)x_1
POL(MARK(x1)) = (4)x_1
POL(g(x1)) = 4 + (4)x_1
POL(h(x1)) = 2 + (1/2)x_1
POL(mark(x1)) = 1/2 + (2)x_1
POL(ACTIVE(x1)) = (4)x_1
g(active(X)) → g(X)
g(mark(X)) → g(X)
h(active(X)) → h(X)
h(mark(X)) → h(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
MARK(h(X)) → ACTIVE(h(X))
MARK(g(X)) → ACTIVE(g(X))
active(g(X)) → mark(h(X))
active(c) → mark(d)
active(h(d)) → mark(g(c))
mark(g(X)) → active(g(X))
mark(h(X)) → active(h(X))
mark(c) → active(c)
mark(d) → active(d)
g(mark(X)) → g(X)
g(active(X)) → g(X)
h(mark(X)) → h(X)
h(active(X)) → h(X)